1. ${\it xm}$ : $\forall$$P$:$\mathbb{P}$. $P$ $\vee$ ($\neg$$P$)
\\[0ex]2. $T$ : Type
\\[0ex]3. $P$ : $T$$\rightarrow\mathbb{P}$
\\[0ex]4. $\exists$$a$:$T$. $P$($a$)
\\[0ex]5. $y$ : $\neg$\{$y$:$T$$\mid$ $P$($y$)\} 
\\[0ex]6. ${\it xm}$(\{$y$:$T$$\mid$ $P$($y$)\} ) = (inr $y$ )
\\[0ex]$\vdash$  "???" $\in$ $T$